feat(recovery): EchoPartialSection + EchoFibreIntersection; wire EchoTruncation (squeakwell R3/R8/R9/R12/R13) - #370

…onest wording; PROOF-STATUS ledger (#80)

## Summary

This PR has four commits.

1. Fixes the Codex review findings that arrived on
[#78](#78)
after it merged. Two were P1: rollback destroyed every batch, and the
Containerfile built nothing. The rest were P2 wording and placeholder
items.
2. Adds the proof ledger `PROOF-STATUS.adoc`, which
README-EXPLAINME-STANDARD section 5 requires before any proof is
claimed. The first rungs of the proof ladder now have prover-checked
artefacts in other repositories.
3. Two rounds of CodeRabbit review fixes. The main ones: batch volumes
each get their own VeriSimDB session, the VeriSimDB URL no longer
appears in logs, and an empty URL now behaves like an unset one. The
ledger's axiom attributions were corrected after a per-lemma re-check.

## Changes

- **P1 rollback (`container/deploy.k9.ncl`)**: each recovery batch runs
on its own named volume `squeakwell-data-<BATCH_ID>`. The default ID is
the UTC time plus the shell's PID, so two batches started in the same
second still differ. Rollback requires `BATCH_ID`, inspects that one
volume and removes only it. The one-line recipes stop with an error if
`BATCH_ID` or `VERISIMDB_URL` is unset.
- **P1 build (`container/Containerfile`, `container/entrypoint.sh`)**: a
wolfi builder stage runs `cargo build --release --locked`, and the
runtime stage copies only the binary. squeakwell is a batch job, so
`EXPOSE`, `HEALTHCHECK` and `APP_PORT` are removed. The entrypoint runs
`/app/squeakwell "$@"`.
- **Per-batch VeriSimDB session (`src/engine/mod.rs`)**: the session ID
is derived from `SQUEAKWELL_BATCH_ID` when it is set. Without this,
every batch mounts its volume at `/data` and they would all share one
session ID. `compose.toml` and the k9 component pass `BATCH_ID` through.
Without a batch ID the session ID still comes from the workdir path, as
before.
- **VeriSimDB URL handling**: the entrypoint logs only the scheme and
host of `VERISIMDB_URL`, with userinfo, path and query stripped. It also
says whether the variable is unset or set to an empty string. The client
treats an empty or blank URL as unset.
- **P2 placeholders**: every `{{TOKEN}}` in `container/` is now filled
in:
  - `manifest.toml`: no listening sockets.
  - `vordr.toml`: no HTTP probe.
  - `compose.toml`: one batch service and one volume per batch.
- `ct-build.sh`, `.gatekeeper.yaml`, `container/README.adoc` and its AI
manifest.
- **Wording**: README, EXPLAINME, `STATE.a2ml`, PROOF-NEEDS and
TEST-NEEDS are corrected:
  - The gate ceiling is L6, and Phase 5 adds no level.
  - VCL-UT gating is planned. The current stub does not invoke the gate.
  - No proof lives in this repo, and the Rust engine is unproved.
- The hub-ceiling results are theory only; how they apply to f64
confidence is open.
  - The Zig FFI template is deleted.
- **`PROOF-STATUS.adoc` (new)**: one row per rung R0–R18, using the
estate status vocabulary and naming the backing artefact. A row is
PROVEN or PROVEN-WITH-AXIOMS only where a prover ran:
- **Rocq:**
[verisimdb#350](hyperpolymath/verisimdb#350).
Each `Print Assumptions` result is recorded per lemma.
- **Agda:**
[echo-types#370](hyperpolymath/echo-types#370).
- **Lean:**
[tropical-types#67](hyperpolymath/tropical-types#67).

R0, R1, R11, R15 and R16 and the Creusot halves are OPEN, and R17 is
ASSUMED. Each row has a receipt giving the toolchain, command and
result.

## Testing

```
cargo test                 # 29 passed, 0 failed
cargo clippy --all-targets # clean
shellcheck -s sh container/entrypoint.sh   # clean
```

Further checks:
- **Container config:** new tests in `tests/container_config_test.rs`
parse compose, manifest and vordr. They pin the batch service shape,
`VERISIMDB_URL`, `SQUEAKWELL_BATCH_ID`, the per-batch volume and its
declaration.
- **k9 one-line recipes:** run with `BATCH_ID` unset they exit 2; with
it set they expand correctly.
- **Entrypoint redaction:** `https://user:s3cret@host:8443/v1?token=abc`
is logged as `https://host:8443`.

Not run here: the image build itself (`podman build`), because podman is
not available in this environment.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8

---------

Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>